constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
internalization and categorical algebra
algebra object (associative, Lie, …)
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
What is called the maybe monad is a simple monad in computer science which is used to implement the most basic kind of “exceptions” indicating the failure of a computation in terms of functional programming: The maybe monad models the exception which witnesses a failure without however producing any further information.
On the type system the maybe monad is the operation of forming the coproduct type with the unit type. (The exception monad for the unit type.)
The idea here is that a function in its Kleisli category is in the original category a function of the form so either returns indeed a value in or else returns the unique element of the unit type/terminal object – it is a partial function. The latter case is naturally interpreted as “no value returned”, hence as indicating a “failure in computation”.
under construction
The Kleisli category of the maybe monad on is the category whose objects are sets, and whose morphisms are partial functions.
This observation generalizes as follows: if is an extensive category and has a terminal object , then a morphism as an object of the overcategory determines (uniquely up to canonical isomorphism) an object
such that , in other words a partial morphism whose domain of definition is a subobject with complement . In brief, maps in the Kleisli category are partial maps with complemented domain.
In particular, in the case of a Boolean topos, the Kleisli category is the category of objects and partial maps; see also partial map classifier.
The algebras over the maybe monad are pointed objects.
Moreover, assuming has finite products and an appropriate form of distributivity (which obtains if for example is lextensive), the maybe monad on is a monoidal monad on the cartesian monoidal category . It follows (by the discussion at commutative monad, see also (Seal 12)) that its Eilenberg-Moore category of algebras canonically inherits the structure of a monoidal category, at least under the mild assumption that it has reflexive coequalizers. Note that the maybe monad preserves reflexive coequalizers, so the monadic functor creates reflexive coequalizers if the base category has them; in this abstract setting the monoidal product on algebras , is given explicitly as the coequalizer of and
where is one of the structural constraints on the monoidal monad and is the multiplication on . One finds that this coequalizer yields the usual smash product of pointed objects.
The smash product as the correct monoidal product can also be deduced in a perhaps more perspicuous manner if we assume more of the base category: that it is cartesian closed, finitely complete, and finitely cocomplete. In that case we construct the internal hom of -algebras, i.e., the internal hom of pointed objects and directly as an equalizer of maps
where the top arrow expresses enriched functoriality of (which in turn is closely related to the strength on ). The success of this is guaranteed by the commutativity of the monad (which here takes a particularly simple form, being given by the commutative monoid with respect to coproduct ). Then, by taking the monoidal product that is adjoint to the internal hom, one is led to the smash product all the same: that is, one can read off the smash product from the fact that pointed maps should correspond to pointed maps .
Regarding just the underlying endofunctor of the maybe monad, its initial algebra over an endofunctor is a natural numbers object.
We may view the augmented simplex category as the subcategory of whose objects are the finite von Neumann ordinals and whose morphisms are the monotone functions between them. Then the maybe monad on restricts to to give the monad that sends the object to and the morphism to the morphism defined by
In fact, is freely generated by this structure and in the sense that its objects are given by , the face maps are given by , the degeneracy maps are given by , and the simplicial identities are precisely the monad axioms. Another way to put this is that is the initial object of the -category whose objects are categories equipped with a monad and an object.
This means that if C is some other category equipped with a comonad and an object then we get a canonical functor and hence an augmented simplicial object in . In particular when is the category of algebras of a monad on we get a simplicial object for each algebra, whose underlying simplicial object in is the bar construction.
The comonad on induces the Décalage comonad.
Around (0.4.24.2) in
the algebraic structure of the would be “field with one element” is regarded as being the maybe monad, hence modules over are defined to be monad-algebras over the maybe monad, hence pointed sets.
Last revised on November 2, 2022 at 08:36:42. See the history of this page for a list of all contributions to it.